Nuprl Lemma : length_segment
2,24
postcript
pdf
T
:Type,
as
:
T
List,
i
:{0...||
as
||},
j
:{
i
...||
as
||}. ||
as
[
i
..
j
]|| =
j
-
i
latex
Definitions
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
nth_tl(
n
;
as
)
,
P
Q
,
P
Q
,
as
[
m
..
n
]
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
...
j
}
Lemmas
int
iseg
wf
,
length
wf1
,
length
firstn
,
nth
tl
wf
,
length
nth
tl
origin
T:Type, as:T List, i:{0...||as||}, j:{i...||as||}. ||as[i..j
]|| = j-i T:Type, as:T List, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i 
Q
A
B
Q Q]
Tx:A. B(x)